$\forall$$l$:IdLnk, $p$:IdLnk List.
\\[0ex]lpath($l$.$p$)
\\[0ex]$\Leftrightarrow$
\\[0ex]lpath($p$)
\\[0ex]\& ($\neg\parallel$$p$$\parallel$ $=$ 0 $\Rightarrow$ destination($l$) $=$ source(hd($p$)) $\in$ Id \& $\neg$hd($p$) $=$ lnk{-}inv($l$) $\in$ IdLnk)